Require Import AutoSep.
Require Import vstte1_header.
Require Import WordLemmas.
Require Import ListLemmas.

(* ============================================================================
 * Module: vstte1
 * ========================================================================= *)

Definition vstte1M :=
  bmodule "vstte1" {{

  bfunction "swap"("a","i","j","t","offset_i","offset_j","a_j") [swapS]
    "offset_i" <- 4 * "i";;
    "t" <-* "a" + "offset_i";;
               
    "offset_j" <- 4 * "j";;
    (*"a" + "offset_i" *<- "a" + "offset_j";;*)
    "a_j" <-* "a" + "offset_j";;
    "a" + "offset_i" *<- "a_j";;

    "a" + "offset_j" *<- "t";;
    Return 0
  end with

  bfunction "sort"("a","s","i","j","offset","val") [sortS]
    "i" <- 0;;
    "j" <- "s";;
    [ Al ls,
      PRE[V] [| allbool ls |] *
             [| length ls = wordToNat (V "s") |] *
             [| (V "i" <= V "j")%word |] *
             [| (wordToNat (V "j") <= length ls)%nat |] *
             array ls (V "a")
      POST[_] array (firstn (wordToNat (V "i")) ls ++
                     sort_bool (skipn (wordToNat (V "i")) (firstn (wordToNat (V "j")) ls)) ++
                     skipn (wordToNat (V "j")) ls) (V "a") ]
    While ("i" < "j") {
      "offset" <- 4 * "i";;
      "val" <-* "a" + "offset";;
      If ("val" = 0) {
        "i" <- "i" + 1
      } else {
        "offset" <- "j" - 1;;
        "offset" <- 4 * "offset";;
        "val" <-* "a" + "offset";;
        If ("val" <> 0) {
           "j" <- "j" - 1
        }
        else {
          "offset" <- "j" - 1;;
          Call "vstte1"!"swap"( "a", "i", "offset" )
          [ Al ls,
            PRE[V] array ls (V "a") * [| allbool ls |] *
                   [| length ls = wordToNat (V "s") |] *
                   [| (V "i" < V "j")%word |] *
                   [| (V "i" ^+ $1 < V "j")%word |] *
                   [| (wordToNat (V "j") <= length ls)%nat |]
            POST[_] array (firstn (wordToNat (V "i") + 1) ls ++
                          sort_bool (skipn ((wordToNat (V "i") + 1)) (firstn ((wordToNat (V "j")) -1) ls)) ++
                          skipn ((wordToNat (V "j")) - 1) ls) (V "a") ];;
          "i" <- "i" + 1;;
          "j" <- "j" - 1
        }
      }
    };;
    Return 0
  end
  }}.

Theorem ok : moduleOk vstte1M.
  vcgen.

  (* for swap function *)
  sep_auto.
  sep_auto.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega);
      assert (sel V "j" < natToW (length ls)) by (evaler; nomega)
  end.
  sep_auto.
  
  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega);
      assert (sel V "j" < natToW (length ls)) by (evaler; nomega)
  end.
  sep_auto.  
  (* end swap function *)

  sep_auto.
  sep_auto.
  sep_auto.
  sep_auto.
  sep_auto.

  nomega.

  unugly.
  rewriter.
  eauto.

  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  sep_auto.

  auto.

  unugly.  
  auto with list.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls)) by (evaler; my_nomega)
  end.

  sep_auto.
  my_nomega.
  my_nomega.
  unugly.
  auto with list.

  sep_auto.
  my2_nomega.
  my2_nomega.
  words.
  unugly.
  auto with list.
  
  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.

  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; my_nomega)
  end.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; my_nomega)
  end.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; my_nomega)
  end.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; my_nomega)
  end.
  sep_auto.
  
  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; my_nomega)
  end.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; my_nomega)
  end.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; rewriter; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; rewriter; my_nomega)
  end.
  sep_auto.

  post.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "i" < natToW (length ls)) by (evaler; rewriter; nomega)
  end.
  match goal with
    | [ V : vals, ls : list W |- _ ] =>
      assert (sel V "j" ^- $1 < natToW (length ls))
        by (evaler; tac_clear; rewriter; my_nomega)
  end.
  sep_auto.
  tac_clear;  nomega.
  tac_clear;  my_nomega.

  auto with list.
  autorewrite with list; auto.
  eauto.
  autorewrite with list; auto.
  words.

  unugly.
  auto with list.

  sep_auto.
  sep_auto.
  sep_auto.
  sep_auto.

  unugly.
  auto with list.
Qed.

Print Assumptions ok.
